A Programming Language for Virtual Double Theories

Abstract: Like familiar theories of first-order logic, the theories of many categorical logics can be specified by a finite presentation of generating symbols and axioms. Each categorical logic is parameterized by a "virtual double theory", a kind of virtual equipment, which can be used to construct type theories over their models. This is especially useful in software systems based on categorical logic, such as CatColab, where models of various domain-specific logics are supported by type systems built uniformly from these virtual double theories.

Building on prior work by Hayato Nasu on a type theory for virtual double categories, we introduce foundations for a programming language for specifying virtual double theories, and present a prototype compiler. We highlight connections with ordered linear logic, and propose a novel operational semantics that captures the universal properties of loose units through a directed reduction procedure.

category theory

Audience: researchers in the topic

Third Virtual Workshop on Double Categories